|
1: |
|
active(app(nil,YS)) |
→ mark(YS) |
2: |
|
active(app(cons(X,XS),YS)) |
→ mark(cons(X,app(XS,YS))) |
3: |
|
active(from(X)) |
→ mark(cons(X,from(s(X)))) |
4: |
|
active(zWadr(nil,YS)) |
→ mark(nil) |
5: |
|
active(zWadr(XS,nil)) |
→ mark(nil) |
6: |
|
active(zWadr(cons(X,XS),cons(Y,YS))) |
→ mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS))) |
7: |
|
active(prefix(L)) |
→ mark(cons(nil,zWadr(L,prefix(L)))) |
8: |
|
active(app(X1,X2)) |
→ app(active(X1),X2) |
9: |
|
active(app(X1,X2)) |
→ app(X1,active(X2)) |
10: |
|
active(cons(X1,X2)) |
→ cons(active(X1),X2) |
11: |
|
active(from(X)) |
→ from(active(X)) |
12: |
|
active(s(X)) |
→ s(active(X)) |
13: |
|
active(zWadr(X1,X2)) |
→ zWadr(active(X1),X2) |
14: |
|
active(zWadr(X1,X2)) |
→ zWadr(X1,active(X2)) |
15: |
|
active(prefix(X)) |
→ prefix(active(X)) |
16: |
|
app(mark(X1),X2) |
→ mark(app(X1,X2)) |
17: |
|
app(X1,mark(X2)) |
→ mark(app(X1,X2)) |
18: |
|
cons(mark(X1),X2) |
→ mark(cons(X1,X2)) |
19: |
|
from(mark(X)) |
→ mark(from(X)) |
20: |
|
s(mark(X)) |
→ mark(s(X)) |
21: |
|
zWadr(mark(X1),X2) |
→ mark(zWadr(X1,X2)) |
22: |
|
zWadr(X1,mark(X2)) |
→ mark(zWadr(X1,X2)) |
23: |
|
prefix(mark(X)) |
→ mark(prefix(X)) |
24: |
|
proper(app(X1,X2)) |
→ app(proper(X1),proper(X2)) |
25: |
|
proper(nil) |
→ ok(nil) |
26: |
|
proper(cons(X1,X2)) |
→ cons(proper(X1),proper(X2)) |
27: |
|
proper(from(X)) |
→ from(proper(X)) |
28: |
|
proper(s(X)) |
→ s(proper(X)) |
29: |
|
proper(zWadr(X1,X2)) |
→ zWadr(proper(X1),proper(X2)) |
30: |
|
proper(prefix(X)) |
→ prefix(proper(X)) |
31: |
|
app(ok(X1),ok(X2)) |
→ ok(app(X1,X2)) |
32: |
|
cons(ok(X1),ok(X2)) |
→ ok(cons(X1,X2)) |
33: |
|
from(ok(X)) |
→ ok(from(X)) |
34: |
|
s(ok(X)) |
→ ok(s(X)) |
35: |
|
zWadr(ok(X1),ok(X2)) |
→ ok(zWadr(X1,X2)) |
36: |
|
prefix(ok(X)) |
→ ok(prefix(X)) |
37: |
|
top(mark(X)) |
→ top(proper(X)) |
38: |
|
top(ok(X)) |
→ top(active(X)) |
|
There are 60 dependency pairs:
|
39: |
|
ACTIVE(app(cons(X,XS),YS)) |
→ CONS(X,app(XS,YS)) |
40: |
|
ACTIVE(app(cons(X,XS),YS)) |
→ APP(XS,YS) |
41: |
|
ACTIVE(from(X)) |
→ CONS(X,from(s(X))) |
42: |
|
ACTIVE(from(X)) |
→ FROM(s(X)) |
43: |
|
ACTIVE(from(X)) |
→ S(X) |
44: |
|
ACTIVE(zWadr(cons(X,XS),cons(Y,YS))) |
→ CONS(app(Y,cons(X,nil)),zWadr(XS,YS)) |
45: |
|
ACTIVE(zWadr(cons(X,XS),cons(Y,YS))) |
→ APP(Y,cons(X,nil)) |
46: |
|
ACTIVE(zWadr(cons(X,XS),cons(Y,YS))) |
→ CONS(X,nil) |
47: |
|
ACTIVE(zWadr(cons(X,XS),cons(Y,YS))) |
→ ZWADR(XS,YS) |
48: |
|
ACTIVE(prefix(L)) |
→ CONS(nil,zWadr(L,prefix(L))) |
49: |
|
ACTIVE(prefix(L)) |
→ ZWADR(L,prefix(L)) |
50: |
|
ACTIVE(app(X1,X2)) |
→ APP(active(X1),X2) |
51: |
|
ACTIVE(app(X1,X2)) |
→ ACTIVE(X1) |
52: |
|
ACTIVE(app(X1,X2)) |
→ APP(X1,active(X2)) |
53: |
|
ACTIVE(app(X1,X2)) |
→ ACTIVE(X2) |
54: |
|
ACTIVE(cons(X1,X2)) |
→ CONS(active(X1),X2) |
55: |
|
ACTIVE(cons(X1,X2)) |
→ ACTIVE(X1) |
56: |
|
ACTIVE(from(X)) |
→ FROM(active(X)) |
57: |
|
ACTIVE(from(X)) |
→ ACTIVE(X) |
58: |
|
ACTIVE(s(X)) |
→ S(active(X)) |
59: |
|
ACTIVE(s(X)) |
→ ACTIVE(X) |
60: |
|
ACTIVE(zWadr(X1,X2)) |
→ ZWADR(active(X1),X2) |
61: |
|
ACTIVE(zWadr(X1,X2)) |
→ ACTIVE(X1) |
62: |
|
ACTIVE(zWadr(X1,X2)) |
→ ZWADR(X1,active(X2)) |
63: |
|
ACTIVE(zWadr(X1,X2)) |
→ ACTIVE(X2) |
64: |
|
ACTIVE(prefix(X)) |
→ PREFIX(active(X)) |
65: |
|
ACTIVE(prefix(X)) |
→ ACTIVE(X) |
66: |
|
APP(mark(X1),X2) |
→ APP(X1,X2) |
67: |
|
APP(X1,mark(X2)) |
→ APP(X1,X2) |
68: |
|
CONS(mark(X1),X2) |
→ CONS(X1,X2) |
69: |
|
FROM(mark(X)) |
→ FROM(X) |
70: |
|
S(mark(X)) |
→ S(X) |
71: |
|
ZWADR(mark(X1),X2) |
→ ZWADR(X1,X2) |
72: |
|
ZWADR(X1,mark(X2)) |
→ ZWADR(X1,X2) |
73: |
|
PREFIX(mark(X)) |
→ PREFIX(X) |
74: |
|
PROPER(app(X1,X2)) |
→ APP(proper(X1),proper(X2)) |
75: |
|
PROPER(app(X1,X2)) |
→ PROPER(X1) |
76: |
|
PROPER(app(X1,X2)) |
→ PROPER(X2) |
77: |
|
PROPER(cons(X1,X2)) |
→ CONS(proper(X1),proper(X2)) |
78: |
|
PROPER(cons(X1,X2)) |
→ PROPER(X1) |
79: |
|
PROPER(cons(X1,X2)) |
→ PROPER(X2) |
80: |
|
PROPER(from(X)) |
→ FROM(proper(X)) |
81: |
|
PROPER(from(X)) |
→ PROPER(X) |
82: |
|
PROPER(s(X)) |
→ S(proper(X)) |
83: |
|
PROPER(s(X)) |
→ PROPER(X) |
84: |
|
PROPER(zWadr(X1,X2)) |
→ ZWADR(proper(X1),proper(X2)) |
85: |
|
PROPER(zWadr(X1,X2)) |
→ PROPER(X1) |
86: |
|
PROPER(zWadr(X1,X2)) |
→ PROPER(X2) |
87: |
|
PROPER(prefix(X)) |
→ PREFIX(proper(X)) |
88: |
|
PROPER(prefix(X)) |
→ PROPER(X) |
89: |
|
APP(ok(X1),ok(X2)) |
→ APP(X1,X2) |
90: |
|
CONS(ok(X1),ok(X2)) |
→ CONS(X1,X2) |
91: |
|
FROM(ok(X)) |
→ FROM(X) |
92: |
|
S(ok(X)) |
→ S(X) |
93: |
|
ZWADR(ok(X1),ok(X2)) |
→ ZWADR(X1,X2) |
94: |
|
PREFIX(ok(X)) |
→ PREFIX(X) |
95: |
|
TOP(mark(X)) |
→ TOP(proper(X)) |
96: |
|
TOP(mark(X)) |
→ PROPER(X) |
97: |
|
TOP(ok(X)) |
→ TOP(active(X)) |
98: |
|
TOP(ok(X)) |
→ ACTIVE(X) |
|
The approximated dependency graph contains 9 SCCs:
{66,67,89},
{68,90},
{69,91},
{73,94},
{70,92},
{71,72,93},
{75,76,78,79,81,83,85,86,88},
{51,53,55,57,59,61,63,65}
and {95,97}.